YES 1.6440000000000001 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((notElem :: (Eq b, Eq a) => (b,a ->  [(b,a)]  ->  Bool) :: (Eq b, Eq a) => (b,a ->  [(b,a)]  ->  Bool)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((notElem :: (Eq a, Eq b) => (a,b ->  [(a,b)]  ->  Bool) :: (Eq a, Eq b) => (a,b ->  [(a,b)]  ->  Bool)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (notElem :: (Eq b, Eq a) => (a,b ->  [(a,b)]  ->  Bool)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xv3400), Succ(xv4001000)) → new_primPlusNat(xv3400, xv4001000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xv30100), Succ(xv400100)) → new_primMulNat(xv30100, Succ(xv400100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xv3000), Succ(xv40000)) → new_primEqNat(xv3000, xv40000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs(@2(xv30, xv31), @2(xv400, xv401), app(app(ty_@2, ba), bb), bc) → new_esEs(xv30, xv400, ba, bb)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), gg), app(ty_Maybe, bbd)), bc) → new_esEs0(xv302, xv4002, bbd)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(ty_Either, hb), hc)), gg), gh), bc) → new_esEs1(xv300, xv4000, hb, hc)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), app(app(ty_Either, bad), bae)), gh), bc) → new_esEs1(xv301, xv4001, bad, bae)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, gg, app(app(ty_@2, bbb), bbc)) → new_esEs(xv302, xv4002, bbb, bbc)
new_esEs1(Right(xv300), Right(xv4000), dh, app(ty_Maybe, ec)) → new_esEs0(xv300, xv4000, ec)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), bcc, app(ty_[], bda)) → new_esEs2(xv31, xv401, bda)
new_esEs(@2(Right(xv300), xv31), @2(Right(xv4000), xv401), app(app(ty_Either, dh), app(app(ty_Either, ed), ee)), bc) → new_esEs1(xv300, xv4000, ed, ee)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, app(ty_Maybe, bac), gh) → new_esEs0(xv301, xv4001, bac)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), gg), app(app(app(ty_@3, bbh), bca), bcb)), bc) → new_esEs3(xv302, xv4002, bbh, bca, bcb)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(ty_[], hd)), gg), gh), bc) → new_esEs2(xv300, xv4000, hd)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], app(ty_Maybe, fd)), bc) → new_esEs0(xv300, xv4000, fd)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(app(ty_@3, he), hf), hg)), gg), gh), bc) → new_esEs3(xv300, xv4000, he, hf, hg)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(app(ty_@2, ge), gf)), gg), gh), bc) → new_esEs(xv300, xv4000, ge, gf)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), app(app(app(ty_@3, bag), bah), bba)), gh), bc) → new_esEs3(xv301, xv4001, bag, bah, bba)
new_esEs0(Just(xv300), Just(xv4000), app(ty_Maybe, bf)) → new_esEs0(xv300, xv4000, bf)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_[], hd), gg, gh) → new_esEs2(xv300, xv4000, hd)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, gg, app(ty_Maybe, bbd)) → new_esEs0(xv302, xv4002, bbd)
new_esEs1(Left(xv300), Left(xv4000), app(app(ty_Either, db), dc), cg) → new_esEs1(xv300, xv4000, db, dc)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), app(ty_[], baf)), gh), bc) → new_esEs2(xv301, xv4001, baf)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_Either, hb), hc), gg, gh) → new_esEs1(xv300, xv4000, hb, hc)
new_esEs(@2(Just(xv300), xv31), @2(Just(xv4000), xv401), app(ty_Maybe, app(app(ty_@2, bd), be)), bc) → new_esEs(xv300, xv4000, bd, be)
new_esEs2(:(xv300, xv301), :(xv4000, xv4001), app(ty_Maybe, fd)) → new_esEs0(xv300, xv4000, fd)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, app(app(ty_Either, bad), bae), gh) → new_esEs1(xv301, xv4001, bad, bae)
new_esEs0(Just(xv300), Just(xv4000), app(app(app(ty_@3, cb), cc), cd)) → new_esEs3(xv300, xv4000, cb, cc, cd)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), gg), app(ty_[], bbg)), bc) → new_esEs2(xv302, xv4002, bbg)
new_esEs1(Right(xv300), Right(xv4000), dh, app(app(ty_@2, ea), eb)) → new_esEs(xv300, xv4000, ea, eb)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), bcc, app(app(ty_Either, bcg), bch)) → new_esEs1(xv31, xv401, bcg, bch)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), bcc, app(app(app(ty_@3, bdb), bdc), bdd)) → new_esEs3(xv31, xv401, bdb, bdc, bdd)
new_esEs(@2(Right(xv300), xv31), @2(Right(xv4000), xv401), app(app(ty_Either, dh), app(ty_Maybe, ec)), bc) → new_esEs0(xv300, xv4000, ec)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_Maybe, ha), gg, gh) → new_esEs0(xv300, xv4000, ha)
new_esEs2(:(xv300, xv301), :(xv4000, xv4001), app(ty_[], fh)) → new_esEs2(xv300, xv4000, fh)
new_esEs(@2(Right(xv300), xv31), @2(Right(xv4000), xv401), app(app(ty_Either, dh), app(app(ty_@2, ea), eb)), bc) → new_esEs(xv300, xv4000, ea, eb)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), bcc, app(app(ty_@2, bcd), bce)) → new_esEs(xv31, xv401, bcd, bce)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), app(ty_Maybe, bac)), gh), bc) → new_esEs0(xv301, xv4001, bac)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, gg, app(ty_[], bbg)) → new_esEs2(xv302, xv4002, bbg)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), gg), app(app(ty_Either, bbe), bbf)), bc) → new_esEs1(xv302, xv4002, bbe, bbf)
new_esEs1(Left(xv300), Left(xv4000), app(app(ty_@2, ce), cf), cg) → new_esEs(xv300, xv4000, ce, cf)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], app(app(app(ty_@3, ga), gb), gc)), bc) → new_esEs3(xv300, xv4000, ga, gb, gc)
new_esEs(@2(Left(xv300), xv31), @2(Left(xv4000), xv401), app(app(ty_Either, app(app(ty_@2, ce), cf)), cg), bc) → new_esEs(xv300, xv4000, ce, cf)
new_esEs0(Just(xv300), Just(xv4000), app(ty_[], ca)) → new_esEs2(xv300, xv4000, ca)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, gg, app(app(app(ty_@3, bbh), bca), bcb)) → new_esEs3(xv302, xv4002, bbh, bca, bcb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, app(app(ty_@2, baa), bab), gh) → new_esEs(xv301, xv4001, baa, bab)
new_esEs1(Left(xv300), Left(xv4000), app(ty_[], dd), cg) → new_esEs2(xv300, xv4000, dd)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), app(app(ty_@2, baa), bab)), gh), bc) → new_esEs(xv301, xv4001, baa, bab)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, hh), gg), app(app(ty_@2, bbb), bbc)), bc) → new_esEs(xv302, xv4002, bbb, bbc)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_@2, ge), gf), gg, gh) → new_esEs(xv300, xv4000, ge, gf)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], app(app(ty_Either, ff), fg)), bc) → new_esEs1(xv300, xv4000, ff, fg)
new_esEs(@2(@3(xv300, xv301, xv302), xv31), @2(@3(xv4000, xv4001, xv4002), xv401), app(app(app(ty_@3, app(ty_Maybe, ha)), gg), gh), bc) → new_esEs0(xv300, xv4000, ha)
new_esEs(@2(Just(xv300), xv31), @2(Just(xv4000), xv401), app(ty_Maybe, app(app(app(ty_@3, cb), cc), cd)), bc) → new_esEs3(xv300, xv4000, cb, cc, cd)
new_esEs(@2(xv30, xv31), @2(xv400, xv401), bcc, app(ty_Maybe, bcf)) → new_esEs0(xv31, xv401, bcf)
new_esEs1(Right(xv300), Right(xv4000), dh, app(app(ty_Either, ed), ee)) → new_esEs1(xv300, xv4000, ed, ee)
new_esEs(@2(Just(xv300), xv31), @2(Just(xv4000), xv401), app(ty_Maybe, app(app(ty_Either, bg), bh)), bc) → new_esEs1(xv300, xv4000, bg, bh)
new_esEs(@2(Left(xv300), xv31), @2(Left(xv4000), xv401), app(app(ty_Either, app(ty_[], dd)), cg), bc) → new_esEs2(xv300, xv4000, dd)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], app(app(ty_@2, fb), fc)), bc) → new_esEs(xv300, xv4000, fb, fc)
new_esEs1(Left(xv300), Left(xv4000), app(ty_Maybe, da), cg) → new_esEs0(xv300, xv4000, da)
new_esEs(@2(Left(xv300), xv31), @2(Left(xv4000), xv401), app(app(ty_Either, app(app(app(ty_@3, de), df), dg)), cg), bc) → new_esEs3(xv300, xv4000, de, df, dg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, app(app(app(ty_@3, bag), bah), bba), gh) → new_esEs3(xv301, xv4001, bag, bah, bba)
new_esEs0(Just(xv300), Just(xv4000), app(app(ty_@2, bd), be)) → new_esEs(xv300, xv4000, bd, be)
new_esEs(@2(Just(xv300), xv31), @2(Just(xv4000), xv401), app(ty_Maybe, app(ty_Maybe, bf)), bc) → new_esEs0(xv300, xv4000, bf)
new_esEs(@2(Left(xv300), xv31), @2(Left(xv4000), xv401), app(app(ty_Either, app(app(ty_Either, db), dc)), cg), bc) → new_esEs1(xv300, xv4000, db, dc)
new_esEs0(Just(xv300), Just(xv4000), app(app(ty_Either, bg), bh)) → new_esEs1(xv300, xv4000, bg, bh)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], gd), bc) → new_esEs2(xv301, xv4001, gd)
new_esEs1(Right(xv300), Right(xv4000), dh, app(app(app(ty_@3, eg), eh), fa)) → new_esEs3(xv300, xv4000, eg, eh, fa)
new_esEs2(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_Either, ff), fg)) → new_esEs1(xv300, xv4000, ff, fg)
new_esEs2(:(xv300, xv301), :(xv4000, xv4001), gd) → new_esEs2(xv301, xv4001, gd)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, app(ty_[], baf), gh) → new_esEs2(xv301, xv4001, baf)
new_esEs2(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_@2, fb), fc)) → new_esEs(xv300, xv4000, fb, fc)
new_esEs(@2(Left(xv300), xv31), @2(Left(xv4000), xv401), app(app(ty_Either, app(ty_Maybe, da)), cg), bc) → new_esEs0(xv300, xv4000, da)
new_esEs(@2(Just(xv300), xv31), @2(Just(xv4000), xv401), app(ty_Maybe, app(ty_[], ca)), bc) → new_esEs2(xv300, xv4000, ca)
new_esEs(@2(Right(xv300), xv31), @2(Right(xv4000), xv401), app(app(ty_Either, dh), app(ty_[], ef)), bc) → new_esEs2(xv300, xv4000, ef)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), hh, gg, app(app(ty_Either, bbe), bbf)) → new_esEs1(xv302, xv4002, bbe, bbf)
new_esEs(@2(Right(xv300), xv31), @2(Right(xv4000), xv401), app(app(ty_Either, dh), app(app(app(ty_@3, eg), eh), fa)), bc) → new_esEs3(xv300, xv4000, eg, eh, fa)
new_esEs(@2(:(xv300, xv301), xv31), @2(:(xv4000, xv4001), xv401), app(ty_[], app(ty_[], fh)), bc) → new_esEs2(xv300, xv4000, fh)
new_esEs1(Right(xv300), Right(xv4000), dh, app(ty_[], ef)) → new_esEs2(xv300, xv4000, ef)
new_esEs2(:(xv300, xv301), :(xv4000, xv4001), app(app(app(ty_@3, ga), gb), gc)) → new_esEs3(xv300, xv4000, ga, gb, gc)
new_esEs1(Left(xv300), Left(xv4000), app(app(app(ty_@3, de), df), dg), cg) → new_esEs3(xv300, xv4000, de, df, dg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(app(ty_@3, he), hf), hg), gg, gh) → new_esEs3(xv300, xv4000, he, hf, hg)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldr(xv3, :(xv40, xv41), ba, bb) → new_foldr(xv3, xv41, ba, bb)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: